Issue892a.agda:11,7-10
R → Set should be a sort, but it isn't
when checking that the expression R.g has type _0
